Hennessy - Milner logic (HML)
構文
論理定項
恆眞$ tt
恆僞$ ff
式の二項演算
連言$ \phi\land\psi
選言$ \phi\lor\psi
式の單項演算
必然$ \lbrack{\rm Act}\rbrack\phi
可能$ \lang{\rm Act}\rang\phi
意味論
遷移を表はす三項關係$ \to~\subseteq S\times{\rm Act}\times S label 付き狀態遷移系 (labeled transition system。labeled state transition system)$ (S,{\rm Act},\to)
label 付き狀態遷移系$ (S,{\rm Act},\to)に對して、狀態と式との二項關係$ \vDash~\subseteq S\times{\rm HML}を定める 狀態は恆眞。$ s\in Sならば$ s\vDash tt
存在しない狀態は恆僞。$ s\notin Sならば$ s\vDash ff
遷移が在れば可能。$ s\xrightarrow{a}s'ならば、$ s'\vDash\phiは$ s\vDash\lang a\rang\phiを導く
遷移に於いて不變ならば必然。狀態$ sと label$ aに對して$ s\xrightarrow{a}s'なる全ての狀態$ s'に於いて$ s'\vDash\phiならば$ s\vDash\lbrack a\rbrack\phi
選言の導入。$ s\vDash\phiならば$ s\vDash\phi\lor\psi。$ s\vDash\psiならば$ s\vDash\phi\lor\psi
連言の導入。$ s\vDash\phi且つ$ s\vDash\psiならば$ s\vDash\phi\land\psi